package arlab.formulae

/**
 * Created by IntelliJ IDEA.
 * User: Eve
 * Date: 23.02.12
 * Time: 12:42
 * To change this template use File | Settings | File Templates.
 */

// Existenzquantor besteht aus einer Variablen und ihrem Scope
case class Exists(x:Variable, a:Formula) extends Formula  {
  override  def toString()={
    "\u2203" + x + ".[" + a.toString() + "]"
  }
  //Funktion gibt alle gebundenen Variablen aus
  override def bound()={
  Set(x) ++ a.bound
  }
  //Hilfsfunktion für die Bestimmung der freien Variablen
  override def freeHelp(bound:Set[Variable]) :Set[Variable]={
    a.freeHelp(bound + x)
  }
  
  
  //gibt eine Liste zurück die Alle Funktionen mitsammt ihren Stelligkeiten zurückgibt.
  override def functions: Set[(String,Int)] = a.functions
  
    
  //substituiert alle Variablen aus der uebergebenen map  
  override def subst(sfn: Map[Variable, Term]): Formula = 
                Exists(x.variant2(sfn.keySet ++ sfn.values), a.subst(Map().updated(x,x.variant2(sfn.keySet ++ sfn.values))).subst(sfn))
}

